import os

import numpy as np
import dfs 
import dpll
import load
import time
from CDCLSolver import CDCLSolver
from test import test_cnf_ans
def sat_solver(path:str):
    '''
    TODO
    返回三元组success,cnf,n
    如果DIMACS文件不规范，success就返回False 在函数中可以打印一些提示信息
    cnf[[3,-5,7],[1,2,-7]]的嵌套列表，3表示命题p3，-5表示命题p5取反，类似于DIMACS格式
    n代表命题数量
    '''
    usedpll = False

    success,cnf,n = load.load_DIMACS(path)
    n = int(n)
    t0 = time.time()
    assert success,'DIMACS不合法'
    #use dpll
    if (usedpll):
        ans = dpll.solve(cnf,n)
        print("cost:",(time.time()-t0)*1000,"ms")
    #use cdcl
    else:
        Solver = CDCLSolver(cnf)
        if Solver.CDCL():
            print("cost:",(time.time()-t0)*1000,"ms")
            print(path+": SAT")
            print("assignment: ", Solver.assignment, "\n")


def test(method:int,path:str):
    success,cnf,n = load.load_DIMACS(path)
    assert success,'DIMACS不合法'
    n = int(n)
    assert(i == 0 or i== 1 or i==2)
    cnf_int = []
    for clause in cnf:
        res = []
        for literal in clause:
            res.append(int(literal))
        cnf_int.append(res)

    if method == 2:
        t0 = time.time()
        Solver = CDCLSolver(cnf,n)
        Solver.CDCL()
        ans = Solver.ans
        delta_t = (time.time()-t0)*1000

        assert test_cnf_ans(cnf_int,ans),'cdcl '+path
        return delta_t
    if method == 0:
        t0 = time.time()
        ans = dfs.solve(cnf_int,n)
        delta_t = (time.time()-t0)*1000
        # print("dfs",ans)
        assert test_cnf_ans(cnf_int,ans),'dfs '+path
        return delta_t
    if method == 1:
        t0 = time.time()
        ans = dpll.solve(cnf_int,n)
        delta_t = (time.time()-t0)*1000
        # print("dpll",ans)
        assert test_cnf_ans(cnf_int,ans),'dpll '+path
        return delta_t




if __name__ == "__main__":
    ## 11111111111
    # path = "C:/project/sat_solver/code/input/uf20-91/uf20-03.cnf"
    # sat_solver(path)
    ## 11111111111

    # root_path = "C:/project/sat_solver/code/input/uf50-218" 
    root_path = "./input/uf20-91"
    # root_path = "./input/uf50-218"
    leftN = 0 
    rightN = 600
    num = 0 
    time_list = [[],[],[]] 
    method_list = ["dfs","dpll","cdcl"] 
    for file in os.listdir(root_path) :
        num+=1
        if(num < leftN):
            continue
        if(num > rightN):
            break
        if num%50 == 0:
            print(file,num)
        path = root_path + '/' + file
        for i in range(0,3):
            _t = test(i,path)
            time_list[i].append(_t)

    for i in range(0,3):
        print(method_list[i])
        print("mean:",np.mean(time_list[i]),"ms")
        print("std:",np.std(time_list[i]),"ms")
        print("------------")
